T:Type, P:(TProp). agree_on(T;a.P(a))  (T List)(T List)Prop 

latex

Definitions	t  T, Prop, ||as||, P  Q, False, A, P & Q, AB, i  j < k, {i..j}, x:A. B(x), l[i], x(s), P  Q, A & B, agree_on(T;x.P(x))
Lemmas	length wf1, int seg wf, select wf